/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.type;

import alloy.ast.EmptyExpr;
import alloy.ast.EmptySetExpr;
import alloy.ast.LeafExpr;
import alloy.util.ObjID;

/**
   Represents the empty type in Alloy.  This class is a singleton which represents
   both the explicitly assigned empty type (i.e. the type of Alloy constant "none") 
   and the empty type that is a result of a type error.  Note that we don't need to
   separate singleton memebers of this class for "none" and "error" since we won't 
   try to continue computing once an error is encountered (e.g. if we have (none->A).B,
   none->A will be reported, and the typechecking of the enclosing formula will be 
   aborted.  If A and B don't intersect, the user will find out about that error after
   fixing the none->A).
*/
final public class EmptyType extends ObjID implements BasicType {
    //NOTE:  I'm leaving the old EMPTY_TYPE stuff in this file and in UnionType.java, RelationType.java, 
    // SigType.java and IntType.java, commented, just in case 
    // we need it in the future . . .

    /** The EmptyType instance (e.g. the type of Alloy constant "none")**/
    public static final EmptyType EMPTY_TYPE = new EmptyType();
    //public static final EmptyType EMPTY_TYPE = new EmptyType(false);

    /** The empty type resulting from a type error (e.g. the type of none & A) **/
    //public static final EmptyType EMPTY_ERROR_TYPE = new EmptyType(true);

    /** flag indicating whether this EmptyType is a result of a type error, or an 
     * explicity assigned EmptyType (i.e. the type of none) **/
    //private final boolean _error;

    /** cannot instantiate new EmptyTypes outside of class */
    //private EmptyType(boolean error_) {_error = error_;}

    /** cannot instantiate new EmptyTypes outside of class */
    private EmptyType() {}

    public LeafExpr toExpr() {
	/**
        QualifiedName emptyName = new QualifiedName(Location.UNKNOWN,
                                                  new Id(Location.UNKNOWN, toString()),
                                                  new Path());
        SigExpr ret = new SigExpr(Location.UNKNOWN, emptyName);
        ret.setType(new UnionType(new RelationType(this)));
	**/
	EmptySetExpr none = new EmptySetExpr(new EmptyExpr());
	none.getTypeExpr().setType(new UnionType(new RelationType(this)));
	none.setType(none.getTypeExpr().getType());
        return none;
    }

    /** Throws an UnsupportedOperationException since 
	the EmptyType cannot contain any atoms **/
    public String getAtomName(int atom_) {
	throw new UnsupportedOperationException();
    }

    public alloy.api.Atom getAtom(int i) {
	throw new UnsupportedOperationException();
    }
    
    public int getScope() {
	throw new UnsupportedOperationException();
    }

    /** EmptyType is a subset of every basic type, so this method always returns true (?) **/
    public boolean isSubtypeOf(BasicType other) {
	return true;
    }

    /** The intersection of EmptyType and every other type is the EMPTY_ERROR_TYPE. **/
    public BasicType intersect(BasicType other) {
	//return EMPTY_ERROR_TYPE;
	return EMPTY_TYPE;
    }

    public boolean isEmpty() {
	return true;
    }

    /** @return true if this is a result of an error; false if this is an explicitly assigned EmptyType **/
    /**
    public boolean isError() {
	return _error;
    }
    **/

    public String toShortString() { return toString(); }

    public String toString() {
	//return (isError() ? "EmptyError" : "Empty");
	return "Empty";
    }


    
}
